i:Id, ds:x:Id fp Type, da:k:Knd fp Type, snd:msg-spec(ds;da), upd:update-spec(ds;da), T:Type,
ks:Knd List, a:((k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)T)), x:Id.
x  dom(ds)
 update-spec-decl(upd;ds)
 (k:Knd. (k  ks)  k  dom(da))
 ecl-machine2(i;ds;da;x;T;ks;a;upd) || ecl-machine3(ds;da;x;T;ks;a;snd) 

latex

Definitions

x:A. B(x), P  Q, ecl-machine2(i;ds;da;x;T;ks;a;upd), ecl-machine3(ds;da;x;T;ks;a;snd), t  T, x. t(x), Prop, SQType(T), {T}, State(ds), if b t else f fi, f(x)?z, 1of(t), 2of(t), x,y. t(x;y), Top, true, false, Valtype(da;k), S  T, S  T, P  Q, x(s), P & Q, P  Q, A, update-spec-decl(upd;ds), False, update-spec(ds;da), , x(s1,s2), Unit, Knd,

Lemmas

R-compat-Rall, IdLnk wf, remove-repeats wf, idlnk-deq wf, msg-spec-links wf, R-lnk-tags wf, fpf-join wf, fpf-single wf, ecl-tags wf, ecl-m3 wf, l member wf, ecl-machine2 wf, R-compat-Rall2, update-spec-vars wf, Knd wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, update-spec-decl wf, not wf, Id wf, id-deq wf, nat wf, decl-state wf, ma-valtype wf, bool wf, update-spec wf, msg-spec wf, fpf wf, R-state-var wf, fpf-ap wf, fpf-compatible-join2, fpf-compatible-single-iff, fpf-compatible-singles, Id sq, list accum wf, subtype rel dep function, fpf-cap wf, top wf, subtype rel self, fpf-cap-join-subtype, fpf-join-cap-sq, fpf-cap-single, eqof eq btrue, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot, R-state-var-lnk-tags-compat2, rcv wf, fpf-cap-void-subtype, deq wf, fpf-compatible-join, fpf-compatible-self